Nuprl Lemma : mon_ident_q
11,40
postcript
pdf
a
:rationals. ((
a
+ 0) =
a
)
((0 +
a
) =
a
)
latex
Definitions
t
T
,
imon{i:l}
,
t
.2
,
t
.1
,
prop{i:l}
,
mon{i:l}
,
grp{i:l}
,
abgrp{i:l}
,
qadd_grp
,
grp_id(
g
)
,
grp_op(
g
)
,
x
f
y
,
grp_car(
g
)
,
P
Q
,
x
:
A
.
B
(
x
)
Lemmas
abgrp
wf
,
grp
id
wf
,
grp
op
wf
,
grp
car
wf
,
monoid
p
wf
,
qadd
grp
wf
,
mon
ident
origin
a:rationals. ((a + 0) = a) 
((0 + a) = a) a:rationals. ((a + 0) = a) ((0 + a) = a) 
T Qx:A. B(x)